perm filename PERMP[EKL,SYS] blob
sn#864133 filedate 1988-08-04 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00015 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00003 00002 functions as lists of numbers
C00006 00003 a list of the lemmata and theorems proved
C00015 00004 PROOFS
C00016 00005 composition of permutation is a permutation
C00022 00006 composition is associative ***try again***
C00027 00007 composition associativity
C00032 00008 uniqueness of composition
C00034 00009 id implies perm
C00036 00010 right identity
C00038 00011 left identity
C00041 00012 the theorem inverse right
C00057 00013 lemma inv implies into
C00060 00014 inv implies perm
C00063 00015 the theorem inverse left
C00070 ENDMK
C⊗;
;functions as lists of numbers
(wipe-out)
(get-proofs appl prf ekl sys)
;definitions of composition,identity, inverse as predicates
(proof comp_pred)
;composition of functions
(decl (comp) (type: |ground⊗ground⊗ground→truthval|) (syntype: constant)
(bindingpower: 930))
(define comp |∀u v w.comp(u,v,w)≡
length u=length w∧(∀n.n<length u⊃nth(u,n)=nth(v,nth(w,n)))|)
(label compdef)
;the identity function
(decl (id) (type: |ground→truthval|))
(defax id |∀u.id(u)≡(∀n.n<length u⊃nth(u,n)=n)|)
(label id_def)
;the inverse of a function
(decl (inv) (type: |ground⊗ground→truthval|))
(defax inv |∀u v.inv(u,v)≡(∀n.n<length u⊃nth(u,n)=fstposition(v,n))|)
(label invdef)
;a list of the lemmata and theorems proved
(proof comp)
;composition
(axiom |∀u v w.perm(v)∧perm(w)∧length v=length w∧comp(u,v,w)⊃perm(u)|)
(label perm_composition)
(axiom |∀u u1 v w.comp(u,v,w)∧comp(u1,v,w)⊃u=u1|)
(label comp_uniqueness)
;identity
(axiom |∀u.id(u)⊃perm(u)|)
(label id_perm)
(axiom |∀u v w.id(u)∧comp(v,w,u)∧length w=length u⊃v=w|)
(label id_right)
(axiom |∀u v w.id(u)∧perm(w)∧length w=length u∧comp(v,u,w)⊃w=v|)
(label id_left)
;inverse right
(axiom |∀u v w.perm(w)∧inv(u,w)∧comp(v,w,u)∧length u=length w⊃id(v)|)
(label inv_right)
;inverse left
(axiom |∀u.perm(u)⊃inj(u)|)
(label perm_injectivity)
;for a proof of this, see the file mult[prm,glb]
(axiom |∀u v.perm(u)∧inv(v,u)∧length v=length u⊃into(v)|)
(label inv_into)
(axiom |∀u v.perm(u)∧inv(v,u)∧length v=length u⊃perm(v)|)
(label inv_perm)
(axiom |∀u v w.perm(w)∧inv(u,w)∧comp(v,u,w)∧length u=length w⊃id(v)|)
(label inverse_left)
(save-proofs permp)
;PROOFS
;composition of permutation is a permutation
(wipe-out)
(get-proofs permp prf ekl sys)
(proof comp_perm)
1. (assume |perm(v)|)
(label cp_pm1)
2. (assume |perm(w)|)
(label cp_pm2)
3. (assume |length v=length w|)
(label cp_pm3)
4. (assume |comp(u,v,w)|)
(label cp_pm4)
;rewrite
5. (rw cp_pm1 (open perm into onto))
;(∀N.N<LENGTH V⊃NATNUM(NTH(V,N))∧NTH(V,N)<LENGTH V)∧(∀N.N<LENGTH V⊃MEMBER(N,V))
(label cp_pm5)
6. (rw cp_pm2 (open perm into onto))
;(∀N.N<LENGTH W⊃NATNUM(NTH(W,N))∧NTH(W,N)<LENGTH W)∧(∀N.N<LENGTH W⊃MEMBER(N,W))
(label cp_pm6)
7. (rw cp_pm4 (open comp ))
;LENGTH U=LENGTH W∧(∀N.N<LENGTH U⊃NTH(U,N)=APPL(V,NTH(W,N)))
(label cp_pm7)
;straightforward verification
8. (assume |m<length(u)|)
(label cp_pm8)
9. (rw * (use cp_pm7 mode: always))
;M<LENGTH W
(label cp_pm9)
10. (derive |NATNUM(NTH(W,M))∧NTH(W,M)<LENGTH V| (cp_pm6 *)
(use cp_pm3 mode: exact))
;so we can obtain the desired result
11. (trw |NATNUM(NTH(V,NTH(W,M)))∧NTH(V,NTH(W,M))<LENGTH V| (* cp_pm5))
(label cp_pm10)
;... and open appl in cp_pm7
12. (derive |nth(u,m)=nth(v,nth(w,m))| (cp_pm7 cp_pm8)
(open appl)(use -2))
13. (rw cp_pm10 (use * mode: exact direction: reverse))
;NATNUM(NTH(U,M))∧NTH(U,M)<LENGTH V
(label cp_pm11)
14. (trw |length u=length v| (use cp_pm7 cp_pm3 mode: always))
;LENGTH U=LENGTH V
(label cp_pm12)
15. (rw cp_pm11 (use * mode: exact direction: reverse))
;NATNUM(NTH(U,M))∧NTH(U,M)<LENGTH U
;deps: (CP_PM1 CP_PM2 CP_PM3 CP_PM4 CP_PM8)
16. (ci cp_pm8)
;M<LENGTH U⊃NATNUM(NTH(U,M))∧NTH(U,M)<LENGTH U
17. (trw |into u| (open into) *)
(label cp_into)
;INTO(U)
;deps: (CP_PM1 CP_PM2 CP_PM3 CP_PM4)
;;;;second part
18. (rw cp_pm8 (use cp_pm12 mode: exact))
;M<LENGTH V
19. (trw |member(m,v)| (* cp_pm5))
;MEMBER(M,V)
(label cp_pm20)
20. (derive |∃j.j<length(v)∧nth(v,j)=m| (* member_nth))
(label cp_pm21)
;deps: (CP_PM1 CP_PM3 CP_PM4 CP_PM8)
21. (define jv |jv<length(v)∧nth(v,jv)=m| *)
(label cp_pm22)
22. (rw * (use cp_pm3 mode: exact))
;JV<LENGTH W∧NTH(V,JV)=M
23. (trw |member(jv,w)| (* cp_pm6))
;MEMBER(JV,W)
24. (derive |∃k.k<length(w)∧nth(w,k)=jv| (* member_nth))
;deps: (CP_PM1 CP_PM2 CP_PM3 CP_PM4 CP_PM8)
25. (define kv |kv<length(w)∧nth(w,kv)=jv| *)
(label cp_pm23)
26. (rw cp_pm22 (use * mode: always direction: reverse))
;NTH(W,KV)<LENGTH V∧NTH(V,NTH(W,KV))=M
(label cp_pm24)
27. (trw |kv<length(u)| cp_pm23 (use cp_pm7 mode: always))
;KV<LENGTH U
(label cp_pm25)
28. (trw |natnum nth(w,kv)| cp_pm23)
;NATNUM(NTH(W,KV))
29. (derive |nth(u,kv)=nth(v,nth(w,kv))| (cp_pm7 cp_pm25)(open appl)(use *))
30. (rw * (use cp_pm24))
;NTH(U,KV)=M
;the last equation allows us to apply lemma nthmember
31. (derive |member(m,u)| nthmember cp_pm25 (use * mode: exact direction: reverse))
;deps: (CP_PM1 CP_PM2 CP_PM3 CP_PM4 CP_PM8)
32. (ci cp_pm8)
;M<LENGTH U⊃MEMBER(M,U)
(label cp_onto)
33. (trw |perm u| (open perm onto) cp_into cp_onto)
;PERM(U)
;deps: (CP_PM1 CP_PM2 CP_PM3 CP_PM4)
34. (ci (CP_PM1 CP_PM2 CP_PM3 CP_PM4))
;PERM(V)∧PERM(W)∧LENGTH V=LENGTH W∧COMP(U,V,W)⊃PERM(U)
(label perm_composition)
;composition is associative ***try again***
(proof comp_associative)
1. (assume |into(w3)|)
(label ca1)
2. (assume |length u=length w3|)
(label ca2)
3. (assume |length u1=length v1|)
(label ca3)
4. (assume |length v1=length w3|)
(label ca4)
5. (assume |length v=length w2|)
(label ca5)
6. (assume |length w2=length w3|)
(label ca6)
7. (assume |comp(u,v,w3)|)
(label ca7)
8. (assume |comp(u1,w1,v1)|)
(label ca8)
9. (assume |comp(v,w1,w2)|)
(label ca9)
10. (assume |comp(v1,w2,w3)|)
(label ca10)
11. (assume |n<length u|)
(label ca11)
12. (rw ca11 (use ca2 mode: exact))
;N<LENGTH W3
(label ca12)
13. (rw ca1 (open into))
;∀N.N<LENGTH W3⊃NATNUM(NTH(W3,N))∧NTH(W3,N)<LENGTH W3
14. (derive |natnum nth(w3,n)∧nth(w3,n)<length w3| (* ca12))
(label ca13)
15. (rw * (use ca6 ca5 mode: exact direction: reverse))
;NATNUM(NTH(W3,N))∧NTH(W3,N)<LENGTH V
(label ca14)
16. (rw ca9 (open comp) ca5)
;∀N.N<LENGTH V⊃NTH(V,N)=NTH(W1,NTH(W2,N))
17. (ue (n |nth(w3,n)|) * ca14)
;NTH(V,NTH(W3,N))=NTH(W1,NTH(W2,NTH(W3,N)))
(label ca15)
18. (rw ca7 (open comp) ca2)
;∀N.N<LENGTH U⊃NTH(U,N)=NTH(V,NTH(W3,N))
19 (ue (n n) * ca11 (use ca15 mode: exact))
;NTH(U,N)=NTH(W1,NTH(W2,NTH(W3,N)))
(label ca16)
;deps: (ca1 CA2 CA5 CA6 CA7 CA9 CA11)
;;;;;;
20. (rw ca12 (use ca4 mode: exact direction: reverse))
;N<LENGTH V1
(label ca20)
21. (rw ca10 (open comp) ca4)
;∀N.N<LENGTH V1⊃NTH(V1,N)=NTH(W2,NTH(W3,N))
;deps: (CA4 CA10)
22. (ue (n n) * ca20)
;NTH(V1,N)=NTH(W2,NTH(W3,N))
(label ca21)
23. (rw ca20 (use ca3 mode: exact direction: reverse))
;N<LENGTH U1
(label ca22)
24. (rw ca8 (open comp) ca3)
;∀N.N<LENGTH U1⊃NTH(U1,N)=NTH(W1,NTH(V1,N))
;deps: (CA3 CA8)
25. (ue (n n) * ca22 (use ca21 mode: exact))
;NTH(U1,N)=NTH(W1,NTH(W2,NTH(W3,N)))
(label ca23)
;deps: (CA3 CA4 CA8 CA11 CA10)
;;;;;;;
26. (trw |nth(u,n)=nth(u1,n)| (use ca16 ca23 mode: exact))
;NTH(U,N)=NTH(U1,N)
;deps: (CA1 CA2 CA3 CA4 CA5 CA6 CA7 CA8 CA9 CA10 CA11)
27. (ci ca11)
;N<LENGTH U⊃NTH(U,N)=NTH(U1,N)
;deps: (CA1 CA2 CA3 CA4 CA5 CA6 CA7 CA8 CA9 CA10)
;labels: EXTENSIONALITY
;(AXIOM |∀U V.LENGTH U=LENGTH V∧(∀I.I<LENGTH U⊃APPL(U,I)=APPL(V,I))⊃U=V|)
28. (ue ((u.u)(v.u1)) extensionality
(use ca2 ca3 ca4 mode: exact) (open appl) *)
;U=U1
;deps: (CA1 CA2 CA3 CA4 CA5 CA6 CA7 CA8 CA9 CA10)
29. (ci (ca1 ca2 ca3 ca4 ca5 ca6 ca7 ca8 ca9 ca10))
;INTO(W3)∧LENGTH U=LENGTH U1∧LENGTH U=LENGTH V1∧LENGTH U=LENGTH V∧
;LENGTH U=LENGTH W2∧LENGTH U=LENGTH W3∧COMP(U,V,W3)∧COMP(U1,W1,V1)∧
;COMP(V,W1,W2)∧COMP(V1,W2,W3)⊃U=U1
;composition associativity
(wipe-out)
(get-proofs permp prf ekl sys)
(proof comp_associative)
1. (assume |into(w3)|)
(label ca1)
2. (assume |length w2=length w3|)
(label ca2)
3. (assume |comp(v,w1,w2)|)
(label ca3)
4. (assume |comp(u,v,w3)|)
(label ca4)
5. (assume |comp(v1,w2,w3)|)
(label ca5)
6. (assume |comp(u1,w1,v1)|)
(label ca6)
7. (assume |n<length u|)
(label ca7)
8. (rw ca4 (open comp))
;LENGTH U=LENGTH W3∧(∀N.N<LENGTH U⊃NTH(U,N)=NTH(V,NTH(W3,N)))
(label ca8)
;deps: (CA4)
9. (derive |n<length(w3)| (ca7 ca8))
(label ca9)
;deps: (CA4 CA7)
10. (derive |nth(u,n)=nth(v,nth(w3,n))| (ca7 ca8))
(label ca10)
;deps: (CA4 CA7)
11. (rw ca1 (open into))
;∀N.N<LENGTH W3⊃NATNUM(NTH(W3,N))∧NTH(W3,N)<LENGTH W3
;deps: (CA1)
12. (derive |natnum(nth(w3,n))∧nth(w3,n)<length(w2)| (ca9 * ca2))
(label ca11)
;deps: (CA1 CA2 CA4 CA7)
13. (rw ca3 (open comp))
;LENGTH V=LENGTH W2∧(∀N.N<LENGTH V⊃NTH(V,N)=NTH(W1,NTH(W2,N)))
(label ca12)
;deps: (CA3)
14. (derive |nth(w3,n)<length(v)| (ca11 ca12))
(label ca13)
;deps: (CA1 CA2 CA3 CA4 CA7)
15. (derive |∀n.n<length(v)⊃nth(v,n)=nth(w1,nth(w2,n))| ca12)
(ue (n |nth(w3,n)|) * ca11 ca13)
;NTH(V,NTH(W3,N))=NTH(W1,NTH(W2,NTH(W3,N)))
;deps: (CA1 CA2 CA3 CA4 CA7)
16. (rw ca10 (use * mode: exact))
;NTH(U,N)=NTH(W1,NTH(W2,NTH(W3,N)))
(label ca14)
;deps: (CA1 CA2 CA3 CA4 CA7)
;;;;;
17. (rw ca5 (open comp))
(label ca20)
;LENGTH V1=LENGTH W3∧(∀N.N<LENGTH V1⊃NTH(V1,N)=NTH(W2,NTH(W3,N)))
18. (derive |nth(v1,n)=nth(w2,nth(w3,n))| (ca9 ca20))
(label ca21)
;deps: (CA4 CA5 CA7)
19. (rw ca6 (open comp))
;LENGTH U1=LENGTH V1∧(∀N.N<LENGTH U1⊃NTH(U1,N)=NTH(W1,NTH(V1,N)))
(label ca22)
;deps: (CA6)
20. (rw ca9 (use ca20 ca22 mode: always direction: reverse))
;N<LENGTH U1
;deps: (CA4 CA5 CA6 CA7)
21. (derive |nth(u1,n)=nth(w1,nth(v1,n))| (ca22 *))
;deps: (CA4 CA5 CA6 CA7)
22. (rw * (use ca21 mode: exact))
;NTH(U1,N)=NTH(W1,NTH(W2,NTH(W3,N)))
(label ca23)
;deps: (CA4 CA5 CA6 CA7)
23. (rw ca14 (use ca23 mode: exact direction: reverse))
;NTH(U,N)=NTH(U1,N)
;deps: (CA1 CA2 CA3 CA4 CA5 CA6 CA7)
24. (ci ca7)
;N<LENGTH U⊃NTH(U,N)=NTH(U1,N)
(label ca24)
;deps: (CA1 CA2 CA3 CA4 CA5 CA6)
25. (trw |length u = length u1| (use ca8 ca22 mode: always)
(use ca20 mode: always direction: reverse))
;LENGTH U=LENGTH U1
;deps: (CA4 CA5 CA6)
;labels: EXTENSIONALITY
;∀U V.LENGTH U=LENGTH V∧(∀I.I<LENGTH U⊃APPL(U,I)=APPL(V,I))⊃U=V
26. (ue ((u.u)(v.u1)) extensionality ca24 *)
;U=U1
;deps: (CA1 CA2 CA3 CA4 CA5 CA6)
27. (ci (ca1 ca2 ca3 ca4 ca5 ca6))
;INTO(W3)∧LENGTH W2=LENGTH W3∧
;COMP(V,W1,W2)∧COMP(U,V,W3)∧
;COMP(V1,W2,W3)∧COMP(U1,W1,V1)⊃U=U1
;uniqueness of composition
(proof uniquecomp)
1. (trw |COMP(U,V,W)∧COMP(U1,V,W)⊃U=U1| (open comp) extensionality)
;COMP(U,V,W)∧COMP(U1,V,W)⊃U=U1
(label comp_uniqueness)
;id implies perm
(proof idperm)
1. (trw |ID(U)⊃INTO(U)| (open id into))
;ID(U)⊃INTO(U)
(label p_i1)
;verification of ontoness is almost as trivial
2. (assume |id(u)|)
(label p_i2)
3. (rw * (open id))
;∀N.N<LENGTH U⊃NTH(U,N)=N
(label p_i3)
4. (assume |n<length u|)
(label p_i4)
5. (derive |member(nth(u,n),u)| (* nthmember))
6. (derive |member(n,u)| (* p_i4 p_i3))
7. (ci p_i4)
;N<LENGTH U⊃MEMBER(N,U)
8. (derive |perm u| (p_i1 p_i2 *) (open perm onto))
9. (ci p_i2)
;ID(U)⊃PERM(U)
(label id_perm)
;right identity
(proof identity_right)
1. (assume |id(u)|)
(label id_r1)
2. (assume |comp(v,w,u)|)
(label id_r2)
3. (assume |length w=length u|)
(label id_r3)
4. (rw id_r1 (open id))
;∀N.N<LENGTH U⊃NTH(U,N)=N
(label id_r4)
5. (rw id_r2 (open comp))
;LENGTH V=LENGTH U∧(∀N.N<LENGTH U⊃NTH(V,N)=NTH(W,NTH(U,N)))
(label id_r5)
6. (rw * (use id_r4 mode: always))
;LENGTH V=LENGTH U∧(∀N.N<LENGTH U⊃NTH(V,N)=NTH(W,N))
(label id_r6)
7. (trw |length v=length w| (use id_r3 id_r5 mode: always))
;LENGTH V=LENGTH W
8. (derive |v=w| (extensionality id_r6 *))
9. (ci (ID_R1 ID_R2 ID_R3))
;ID(U)∧COMP(V,W,U)∧LENGTH W=LENGTH U⊃V=W
;left identity
(proof identity_left)
1. (assume |id(u)|)
(label id_l1)
2. (assume |perm w|)
(label id_l2)
3. (assume |length w=length u|)
(label id_l3)
4. (assume |comp(v,u,w)|)
(label id_l4)
5. (rw id_l1 (open id))
;∀N.N<LENGTH U⊃NTH(U,N)=N
(label id_l5)
6. (rw id_l4 (open comp))
;LENGTH V=LENGTH W∧(∀N.N<LENGTH V⊃NTH(V,N)=NTH(U,NTH(W,N)))
(label id_l6)
7. (rw id_l2 (open perm onto into))
;(∀N.N<LENGTH W⊃NATNUM(NTH(W,N))∧NTH(W,N)<LENGTH W)∧(∀N.N<LENGTH W⊃MEMBER(N,W))
(label id_l7)
8. (trw |∀M.M<LENGTH U⊃NATNUM(NTH(W,M))∧NTH(W,M)<LENGTH U| id_l7
(use id_l3 mode: exact direction: reverse))
;∀M.M<LENGTH U⊃NATNUM(NTH(W,M))∧NTH(W,M)<LENGTH U
(label id_l8)
;so we can apply the property of the identity function u
9. (trw |∀M.M<LENGTH U⊃NTH(U,NTH(W,M))=NTH(W,M)| id_l5 * )
;∀M.M<LENGTH U⊃NTH(U,NTH(W,M))=NTH(W,M)
(label id_l9)
;we will use extensionality
10. (assume |m<length v|)(label id_l10)
11. (trw |m<length u| * (use id_l3 id_l6 mode: exact direction: reverse))
;M<LENGTH U
(label id_l11)
12. (derive |NTH(U,NTH(W,M))=NTH(W,M)| (id_l9 id_l11))
;so we can apply the fact that V is the composition of U and W
13. (derive |NTH(V,M)=NTH(W,M)| (id_l6 id_l10) (use * mode: exact direction: reverse))
14. (ci id_l10)
;M<LENGTH V⊃NTH(V,M)=NTH(W,M)
15. (derive |W=V| (extensionality id_l6 *))
16. (ci (ID_L1 ID_L2 ID_L3 ID_L4))
;ID(U)∧PERM(W)∧LENGTH W=LENGTH U∧COMP(V,U,W)⊃W=V
;the theorem inverse right
(proof inverse_right)
1. (assume |perm w|)
(label invr1)
2. (assume |inv(u,w)|)
(label invr2)
3. (assume |length u=length w|)
(label invr3)
4. (assume |comp(v,w,u)|)
(label invr4)
;rewrite
5. (rw invr1 (open perm onto into))
;(∀N.N<LENGTH W⊃NATNUM(NTH(W,N))∧NTH(W,N)<LENGTH W)∧(∀N.N<LENGTH W⊃MEMBER(N,W))
(label invr5)
6. (rw invr2 (open inv))
;∀N.N<LENGTH U⊃NTH(U,N)=FSTPOSITION(W,N)
(label invr6)
7. (rw invr4 (open comp))
;LENGTH V=LENGTH U∧(∀N.N<LENGTH U⊃NTH(V,N)=NTH(W,NTH(U,N)))
(label invr7)
8. (assume |m<length v|)(label invr8)
(rw * (use invr7 mode: exact))
;M<LENGTH U
(label invr9)
;use the facts that V is the composition of W and U and that U is the inverse of W
9. (trw |NTH(V,M)=NTH(W,FSTPOSITION(W,M))| (invr7 *)
(use invr6 mode: always direction: reverse))
;NTH(V,M)=NTH(W,FSTPOSITION(W,M))
(label invr10)
10. (rw invr9 (use invr3 mode: exact))
;M<LENGTH W
11. (derive |member(m,w)| (invr5 *))
;so we can apply the lemma nth_fstposition
12. (rw invr10 (use nth_fstposition * mode: always))
;NTH(V,M)=M
13. (ci invr8)
;M<LENGTH V⊃NTH(V,M)=M
14. (trw |id(v)| (open id) *)
;ID(V)
15. (ci (INVR1 INVR2 INVR4 INVR3))
;PERM(W)∧INV(U,W)∧COMP(V,W,U)∧LENGTH U=LENGTH W⊃ID(V)
;lemma inv implies into
(wipe-out)
(get-proofs permp prf ekl sys)
(proof inv_into)
1. (assume |perm(u)|)
(label ii1)
2. (assume |inv(v,u)|)
(label ii2)
3. (assume |length v=length u|)
(label ii3)
4. (rw ii1 (open perm into onto) )
(label ii4)
;(∀N.N<LENGTH U⊃NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH U)∧(∀N.N<LENGTH U⊃MEMBER(N,U))
5. (rw ii2 (open inv))
(label ii5)
;∀N.N<LENGTH V⊃NTH(V,N)=FSTPOSITION(U,N)
6. (assume |m<length v|)
(label ii6)
7. (derive |NTH(V,M)=FSTPOSITION(U,M)| (ii5 ii6))
(label ii7)
8. (rw ii6 (use ii3 mode: exact))
;M<LENGTH U
9. (derive |member(m,u)| (* ii4))
;MEMBER(M,U)
10. (trw |natnum fstposition(u,m)∧fstposition(u,m)<length u|
(use pos_length * mode: always) (use posfacts ue: ((u.u)(y.m)) ))
;NATNUM(FSTPOSITION(U,M))∧FSTPOSITION(U,M)<LENGTH U
11. (rw * (use ii3 ii7 mode: exact direction: reverse))
;NATNUM(NTH(V,M))∧NTH(V,M)<LENGTH V
;deps: (II1 II2 II3 II6)
12. (ci ii6)
;M<LENGTH V⊃NATNUM(NTH(V,M))∧NTH(V,M)<LENGTH V
13. (trw |into v| (open into) *)
;INTO(V)
;deps: (II1 II2 II3)
14. (ci (ii1 ii2 ii3))
;PERM(U)∧INV(V,U)∧LENGTH V=LENGTH U⊃INTO(V)
;inv implies perm
(proof inv_onto)
1. (assume |perm u|)
(label io1)
2. (assume |inv(v,u)|)
(label io2)
3. (assume |length v=length u|)
(label io3)
4. (rw io1 (open perm into onto) )
;(∀N.N<LENGTH U⊃NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH U)∧(∀N.N<LENGTH U⊃MEMBER(N,U))
(label io4)
5. (rw io2 (open inv))
;∀N.N<LENGTH V⊃NTH(V,N)=FSTPOSITION(U,N)
(label io5)
6. (derive |∀n.n<length u⊃fstposition(u,nth(u,n))=n|
(fstposition_nth perm_injectivity uniqueness_injectivity io1 io4))
;deps: (IO1)
(label io6)
7. (assume |n<length v|)
(label io7)
8. (rw * (use io3 mode: exact))
;N<LENGTH U
(label io8)
9. (derive |NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH V| (io3 io4 io8))
(label io9)
;deps: (IO1 IO3 IO7)
;so we can use the fact that V is the inverse of U...
10. (trw |NTH(V,NTH(U,N))=FSTPOSITION(U,NTH(U,N))|(io5 *))
;NTH(V,NTH(U,N))=FSTPOSITION(U,NTH(U,N))
(label io10)
;deps: (IO1 IO2 IO3 IO7)
;...the lemma fstposition_nth
11. (rw * (use io6 io8 mode: exact))
;NTH(V,NTH(U,N))=N
;deps: (IO1 IO2 IO3 IO7)
(label io11)
;...the lemma nthmember
12. (trw |member(nth(v,nth(u,n)),v)| (nthmember io9))
;MEMBER(NTH(V,NTH(U,N)),V)
;deps: (IO1 IO3 IO7)
13. (rw * (use io11 mode: exact))
;MEMBER(N,V)
;deps: (IO1 IO2 IO3 IO7)
;...and obtain the second condition for ontoness
14. (ci io7)
;N<LENGTH V⊃MEMBER(N,V)
;deps: (IO1 IO2 IO3)
15. (derive |into v| (inv_into io1 io2 io3))
;deps: (IO1 IO2 IO3)
16. (trw |perm v| (open perm onto) -2 *)
;PERM(V)
;deps: (IO1 IO2 IO3)
17. (ci (IO1 IO2 IO3))
;PERM(U)∧INV(V,U)∧LENGTH V=LENGTH U⊃PERM(V)
;the theorem inverse left
(wipe-out)
(get-proofs permp prf ekl sys)
(proof compose_inverse_left)
1. (assume |perm(w)|)
(label invl_1)
2. (assume |inv(u,w)|)
(label invl_2)
3. (assume |comp(v,u,w)|)
(label invl_3)
4. (assume |length(w)=length(u)|)
(label invl_4)
5. (rw invl_2 (open inv))
;∀N.N<LENGTH U⊃NTH(U,N)=FSTPOSITION(W,N)
(label invl_5)
6. (rw invl_1 (open perm onto into))
;(∀N.N<LENGTH W⊃NATNUM(NTH(W,N))∧NTH(W,N)<LENGTH W)∧
;(∀N.N<LENGTH W⊃MEMBER(N,W))
(label invl_6)
;deps: (INVL_1)
7. (rw invl_3 (open comp))
;LENGTH V=LENGTH W∧(∀N.N<LENGTH V⊃NTH(V,N)=NTH(U,NTH(W,N)))
(label invl_7)
8. (derive |∀n.n<length w⊃fstposition(w,nth(w,n))=n|
(fstposition_nth perm_injectivity uniqueness_injectivity
invl_1 invl_6))
(label invl_8)
;deps: (INVL_1)
9. (rw invl_6 (use invl_4 mode: exact))
;(∀N.N<LENGTH U⊃NATNUM(NTH(W,N))∧NTH(W,N)<LENGTH U)∧
;(∀N.N<LENGTH U⊃MEMBER(N,W))
(label invl_9)
;deps: (INVL_1 INVL_4)
10. (assume |n<length v|)
(label invl_10)
11. (rw * (use invl_7 mode: always))
;N<LENGTH W
(label invl_11)
;deps: (INVL_3 INVL_10)
12. (rw * invl_4)
;N<LENGTH U
(label invl_12)
;deps: (INVL_3 INVL_4 INVL_10)
13. (derive |natnum(nth(w,n))∧nth(w,n)<length u| (invl_9 *))
(label invl_13)
;deps: (INVL_1 INVL_3 INVL_4 INVL_10)
14. (derive |NTH(V,N)=NTH(U,NTH(W,N))| (invl_7 invl_10))
(label invl_14)
;deps: (INVL_3 INVL_10)
15. (rw invl_14 (use invl_5 ue: ((n.|nth(w,n)|)) invl_13 mode: exact))
;NTH(V,N)=FSTPOSITION(W,NTH(W,N))
(label invl_15)
;deps: (INVL_1 INVL_2 INVL_3 INVL_4 INVL_10)
;want to apply the lemma fstposition_nth
16. (rw invl_15 (use invl_8 invl_11 mode: always))
;NTH(V,N)=N
;deps: (INVL_1 INVL_2 INVL_3 INVL_4 INVL_10)
;and so V is the identity function
17. (ci invl_10)
;N<LENGTH V⊃NTH(V,N)=N
;deps: (INVL_1 INVL_2 INVL_3 INVL_4)
18. (trw |id v| (open id) *)
;ID(V)
;deps: (INVL_1 INVL_2 INVL_3 INVL_4)
19. (ci (INVL_1 INVL_2 INVL_3 INVL_4))
;PERM(W)∧INV(U,W)∧COMP(V,U,W)∧LENGTH W=LENGTH U⊃ID(V)
;THEOREM
;PERM(W)∧INV(U,W)∧LENGTH W=LENGTH U⊃ID(U⊗W)
;Proof.Assuming that W is a PERM, that U is the inverse of W, that V is the result
;of composing U and W and the LENGTH W = LENGTH U, we need to prove that
;for all N<LENGTH V, NTH(U⊗W,N)=N.
;Assume N<LENGTH V. After expanding the definitions we know that LENGTH V=LENGTH W,
;so N<LENGTH W and N<LENGTH U.
;Similarly, all members of W are NATNUM less than LENGTH(U) [line invl_12],
;so the sorts are verified and we can apply the definition of composition to get
;NTH(V,N)=NTH(U,NTH(W,N)) [line invl_13], and the definition of INV to obtain
;NTH(U⊗W,N)=FSTPOSITION(W,NTH(W,N)) [line invl_14]
;We want to conclude
;FSTPOSITION(W,NTH(W,N))=N
;This need not be true if in W there are several occurrences of the nth element,
;but W is a PERM, so by the pigeon hole principle W is INJ; therefore we can apply
;the lemma FSTPOSITION_NTH and obtain the desired conclusion.
;labels: INJDEF
;(DEFINE INJ |∀U.INJ(U)=(∀N M.N<LENGTH U∧M<LENGTH U∧APPL(U,N)=APPL(U,M)⊃N=M)| )
;labels: PERM_INJECTIVITY
;(AXIOM |∀U.PERM(U)⊃INJ(U)|)
;labels: FSTPOSITION_NTH
;(AXIOM |∀U N.UNIQUENESS(U)∧MEMBER(N,U)⊃FSTPOSITION(U,NTH(U,N))=N|)